Nuprl Definition : detach_fun
13,42
postcript
pdf
detach_fun(
T
;
A
) == {
d
:
T
|
x
:
T
. (
(
A
(
x
)))
(
(
d
(
x
)))}
latex
Up
gen
algebra
1
Wellformedness Lemmas
detach
fun
wf
Definitions
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
,
x
:
A
.
B
(
x
)
,
P
Q
,
T
,
b
,
f
(
a
)
origin
| 
x:T. (
(A(x))) 
(
(d(x)))} | x:T. ((A(x))) ((d(x)))} B(x)x:A. B(x) QTb